Nuprl Lemma : eq_int_eq_false_elim 13,42

ij:. ((i = j) = ff   i  j 
latex


Upbool 1, bool 1
Definitions, t  T, P  Q, x:AB(x), a  b  T , P  Q, P & Q, P  Q, P  Q, Dec(P), False, A
Lemmasbfalse wf, eq int wf, bool wf, decidable int equal, eq int eq true, btrue neq bfalse

origin